1.1. Field of the Invention
The present invention relates to the field of computer hardware logic circuits, and in particular to a method for verifying the proper operation of a digital logic circuit.
1.2. Description and Disadvantages of Prior Art
Digital logic circuits implement a predetermined logic function of a digital hardware, by processing some input bit vector for producing an output result. Such circuits represent the core of any computing processing unit. Thus, before a logic circuit, or “hardware design” is constructed in hardware, its respective logic simulation model must be tested and the proper operation thereof has to be verified with many different input settings. This is usually done in prior art with simulation of a so-called gate-level netlist. This gate-level netlist has a graph structure with Boolean gates as nets and nets as connecting arcs. Storage elements like latches can be built from Boolean gates and are commonly included as nets in a gate-level netlist. In the following, we assume that a latch is included as a possible net in a gate-level netlist. Also, the abbreviated term “netlist” may be substituted for “gate-level netlist”. This gate-level netlist is representing the respective sections of the desired hardware circuit.
Assume, a simple exemplary circuit has a plurality of 16 input bits. Then, a plurality of 2 exp 16=65536 different input settings exist, which should be tested in total for correct operation of the circuit, or its logic model, respectively. This is already a time-consuming work, either done by a computer, but at least surveyed in critical points within the circuit by the hardware developer engineering team. Thus, this way of hardware verification is called “exhaustive” functional verification.
Today's hardware designs, however, are much more complex than the before-mentioned simple 16-bit circuit. Even single sections of a hardware design may comprise hundreds, or several thousands of input variables.
This enormous input bit setting space cannot be verified in such exhaustive way, covering for example a plurality of (2 exp 2500) different input settings, ie “stimuli”, and their correct propagation through the gate-level netlist. Thus, a so-called “biased, random” verification is done, selecting some bit settings only, the propagation of which seems to touch at least some of the “problematic zones” in a hardware design. Such selection might be to select an input bit pattern consisting of only “0”, one of only “1”, (corner cases), and some randomly selected patterns in-between them, comprising both values. There are also variations in that type of methods in prior art, like “walking 1s”, etc.
In summary, the drawbacks of exhaustive functional verification are:
The simulation runtime is very long due to an exhaustive set of stimuli.
In lots of cases it is a time-consuming work, to check that all possible combinations for example on a certain data path in a gate-level netlist are exercised, and that they work correctly. A full (complete) checking is difficult to perform, since a logic function does not necessarily generate signal level changes, when for example, only one bit is changed in relation to the preceding input bit pattern. This is due to restrictions in the testbench, when registers are being set and reset, but there are only special combinations allowed (i.e. writing zeros to a register that shows already only zeros).
An alternative for doing exhaustive, bit value oriented, functional simulation is the prior art “symbolic” simulation. Here, instead of bit values, symbols are propagated through the gate-level netlist. For example, a 2-input AND gate with input symbols “a” and “b” produces a result “a AND b”. This short logic expression is then the input for another gate, thus, maybe “a AND b OR c” results after the next step in a selected path. A long path in the logic results in an expression of significant extent. If, further, some feedback loop connects between some net location and a preceding net location of the propagation path, such expression can easily “explode”. This is a disadvantageous limitation of symbolic simulation or verification.
In summary, the drawbacks of “symbolic simulation” are:
First, only small designs can be verified due to the possible expression explosion.
Further, such expressions grow dynamically; therefore the simulation cannot be run on so-called hardware accelerators, i.e. on dedicated high-performance simulation servers. Further, as the symbols have no value, a regular, usual bit-value-based functional simulation cannot be carried out simultaneously, which is often strongly desired.
1.3. Objectives of the Invention
It is thus an objective of the present invention to provide a method for verification of logic circuits, which adds a useful alternative in the field of functional, exhaustive simulation and of symbolic simulation.